test_case1()  (( List) + Atom) 

latex

Definitions	x. t(x), T, ff, P  Q, P & Q, P  Q, tt, if b then t else f fi , True, Y, t  ...$L, i  j , ||as||, False, P  Q, A, A  B, , x:A. B(x), , x:A. B(x), t  T, test_case1(), x(s), P  Q, Dec(P), Unit, , , S  T
Lemmas	pi1 wf, assert of le int, bnot of lt int, true wf, squash wf, eqff to assert, assert of lt int, eqtt to assert, iff transitivity, bnot wf, le int wf, non neg length, length cons, length nil, length wf1, int inc rationals, select wf, assert wf, bool wf, lt int wf, le wf, q-constraints wf, decidable wf, rationals wf, nat wf